Issue4121-2.agda:13,5-7
Not in scope:
  c′ at Issue4121-2.agda:13,5-7
    (did you mean 'M.c′'?)
when scope checking c′
